In this letter we give a lower bound on the worst-case time complexity of Dijkstra's three-state mutual exclusion algorithm by specifying a concrete behavior of the algorithm. We also show that our result is more accurate than the known best bound.

A distributed system is said to be self-stabilizing if it converges to some legitimate state from an arbitrary state in a finite number of steps. The number of steps required for convergence is usually referred to as the stabilization time, and its reduction is one of the main performance issues in the design of self-stabilizing systems. In this paper, we propose an automated method for computing the stabilization time. The method uses Boolean functions to represent the state space in order to assuage the state explosion problem, and computes the stabilization time by manipulating the Boolean functions. To demonstrate the usefulness of the method, we apply it to the analysis of existing self-stabilizing algorithms. The results show that the method can perform stabilization time analysis very fast, even when an underlying state space is very huge.

This paper discusses the collection of sensor data for power distribution systems. In current power distribution systems, this is usually performed solely by the Remote Terminal Unit (RTU) which is located at the root of a power distribution network. The recent rise of distributed power sources, such as photovoltaic generators, raises the demand to increase the frequency of data collection because the output of these distributed generators varies quickly depending on the weather. Increasing data collection frequency in turn requires shortening the time required for data collection. The paper proposes the use of aggregation points for this purpose. An aggregation point can collect sensor data concurrently with other aggregation points as well as with the RTU. The data collection time can be shortened by having the RTU receive data from aggregation points, instead of from all sensors. This approach then poses the problem of finding the optimal location of aggregation points. To solve this problem, the paper proposes a Mixed Integer Linear Problem (MILP) formulation of the problem. The MILP problem can then be solved with off-the-shelf mathematical optimization software. The results of experiments show that the proposed approach is applicable to rather large scale power distribution systems.

Model checking is a technique that can make a verification for finite state systems absolutely automatic. We propose a method for automatic verification of fault-tolerant concurrent systems using this technique. Unlike other related work, which is tailored to specific systems, we are aimed at providing an approach that can be used to verify various kinds of systems against fault tolerance. The main obstacle in model checking is state explosion. To avoid the problem, we design this method so that it can use a symbolic model checking tool called SMV (Symbolic Model Verifier). Symbolic model checking can overcome the problem by expressing the state space and the transition relation by Boolean functions. Assuming that a system to be verified is modeled as a guarded command program, we design a modeling language and propose a translation method from the modeling language to the input language of SMV. We show the results of applying the proposed method to various examples to demonstrate the feasibility of the method.